i:Id, ds:x:Id fp Type, da:k:Knd fp Type, T:Type, es:ES.
es-decls(es;i;ds;da)
 vartype(i;"ecl")  T
 "ecl"  dom(ds)
 es-decls(es;i;ds  "ecl" : T;da) 

latex

Definitions	{T}, P  Q, P  Q, P  Q, x:A. B(x), x. t(x), P & Q, t  T, Id, "$x", if b t else f fi, true, Top, false, Prop, f(x)?z, 2of(t), x : v, f(x), SQType(T), x(s), Unit, ,
Lemmas	es-decls-iff, fpf-single wf, es-vartype wf, fpf-join wf, fpf-compatible-join-cap, fpf-compatible-single, id-deq wf, top wf, fpf-dom wf, iff transitivity, bool wf, assert wf, bnot wf, eqtt to assert, eqff to assert, assert of bnot, not wf, Id sq, fpf-single-dom